COMMENT ⊗   VALID 00005 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	the pigeon hole principle
C00003 00003	* using the inductive predicate `all' the theorem comes quickly
C00013 00004	the arithmetical pigeon hole principle: long proof
C00018 00005	the pigeon hole principle on lists
C00038 ENDMK
C⊗;
;the pigeon hole principle
(wipe-out)
(get-proofs mult prf ekl sys)

(proof pigeonfacts)

;the arithmetical form of the pigeon hole principle

(axiom |∀f n.(∀m.m≤n⊃natnum f(m))∧(∀m.m<n⊃1≤f(m))∧sum(λk.f(k),n)≤n⊃(∀m.m<n⊃1=f(m))|)
(label pigeonfact)

;the pigeon hole principle on lists

(axiom |∀setseq u.disjoint(setseq,length u)∧
                  (∀k.k<length u⊃1≤mult(u,setseq(k)))⊃
                  (∀k.k<length u⊃1=mult(u,setseq(k)))|)
(label pigeonlist)

(save-proof pigeon)
;* using the inductive predicate `all' the theorem comes quickly;
    (wipe-out)
    (get-proofs sums prf ekl sys)
    (proof pigeonfact)

1.  (assume |∀n.natnum f(n)|)
    (label sort1)

2.  (ue ((numseq.|λk.f(k)|)(n.n)) sumsort *)
    ;NATNUM(SUM(λK.F(K),N))
    (label sort2)

3.  (ue (a |λn.all(n,λk.1≤f(k))⊃n≤sum(λk.f(k),n)|) 
        proof_by_induction 
        (open all sum)  zeroleast (use sort1 sort2 mode: always)
        (use add_lesseq ue: ((n.n)(k.|f(n)|)(m.|sum(λk.f(k),n)|)) ))
    (label strictly_increasing)
    ;∀N.ALL(N,λK.1≤F(K))⊃N≤SUM(λK.F(K),N)
    ;deps: (SORT1)

4.  (ue (a |λn.all(n,λk.1≤f(k))∧sum(λk.f(k),n)=n⊃all(n,λk.1=f(k))|)
        proof_by_induction (open all sum) strictly_increasing sort1 sort2
        (use add_one ue: ((k.|f(n)|)(n.n)(m.|sum(λk.f(k),n)|)) mode: always))
    ;∀N.ALL(N,λK.1≤F(K))∧SUM(λK.F(K),N)=N⊃ALL(N,λK.1=F(K))

;in more conventional notation:

5.  (rw * (use allfact ue: ((a.|λk.1≤f(k)|)(n.n)) 
               mode: always direction: reverse)
          (use allfact ue: ((a.|λk.1=f(k)|)(n.n)) 
               mode: always direction: reverse))
    ;∀N.(∀M.M<N⊃1≤F(M))∧SUM(λK.F(K),N)=N⊃(∀M.M<N⊃1=F(M))
    ;deps: (SORT1)

6.  (ci sort1)
    ;(∀N.NATNUM(F(N)))⊃
    ;(∀N.(∀M.M<N⊃1≤F(M))∧SUM(λK.F(K),N)=N⊃(∀M.M<N⊃1=F(M)))
;;;;;;
;   (axiom |∀numseq n.all(n,λm.natnum(numseq(m)))⊃natnum(sum(numseq,n))|)
;   (label sumsort1)
;
;   1.  (ue (a |λn.all(n,λk.natnum f(k))∧all(n,λk.1≤f(k))⊃
;		   natnum sum(λk.f(k),n)∧n≤sum(λk.f(k),n)|) 
;	    proof_by_induction 
;	    (open all sum)  zeroleast sumsort1
;	    (use add_lesseq ue: ((n.n)(k.|f(n)|)(m.|sum(λk.f(k),n)|)) ))
;   1. ;∀N.ALL(N,λM.NATNUM(F(M)))∧ALL(N,λK.1≤F(K))⊃N≤SUM(λK.F(K),N)
;	(label strictly_increasing)
;
;   ;doesn't work
;   2.  (ue (a |λn.all(n,λk.natnum f(k))∧all(n,λk.1≤f(k))∧sum(λk.f(k),n)=n⊃
;		   all(n,λk.1=f(k))|)
;	    proof_by_induction (open all sum) 
;	    (use strictly_increasing sumsort1 mode: always)
;	    (use add_one ue: ((k.|f(n)|)(n.n)(m.|sum(λk.f(k),n)|)) mode: always))
;
;the arithmetical pigeon hole principle: long proof
    (wipe-out)
    (get-proofs sums prf ekl sys)

    (proof pigeonfact)

1.  (assume |(∀m.m<n⊃natnum f(m)∧1≤f(m))⊃n≤sum(λk.f(k),n)|)
    (label si_indhyp)

2.  (assume |∀m.m<n'⊃natnum f(m)∧1≤f(m)|)
    (label si_hyp)

3.  (trw |∀m.m<n⊃natnum f(m)∧1≤f(m)| (* transitivity_of_order successor1))
    ;∀M.M<N⊃NATNUM(F(M))∧1≤F(M)
    (label si1)

4.  (ue ((numseq.|λk.f(k)|)(n.n)) sumsort *)
    ;NATNUM(SUM(λK.F(K),N))
    (label sisort)

5.  (derive |n≤sum(λk.f(k),n)|(si1 si_indhyp))
    (label si2)

6.  (ue (m n) si_hyp successor1)
    ;NATNUM(F(N))∧1≤F(N)
    (label si3)
    ;deps: (SI_HYP)

7.  (ue ((n.n)(k.|f(n)|)(m.|sum(λk.f(k),n)|)) add_lesseq (sisort si2 si3))
    ;N'≤SUM(λK.F(K),N)+F(N)
    ;deps: (SI_INDHYP SI_HYP)

8.  (ci si_hyp)
    ;(∀M.M<N'⊃NATNUM(F(M))∧1≤F(M))⊃N'≤SUM(λK.F(K),N)+F(N)
    ;deps: (SI_INDHYP)

9.  (ci si_indhyp)
    ;((∀M.M<N⊃NATNUM(F(M))∧1≤F(M))⊃N≤SUM(λK.F(K),N))⊃
    ;((∀M.M<N'⊃NATNUM(F(M))∧1≤F(M))⊃N'≤SUM(λK.F(K),N)+F(N))

10. (ue (a |λn.(∀m.m<n⊃natnum f(m)∧1≤f(m))⊃n≤sum(λk.f(k),n)|) proof_by_induction 
        (open sum)  zeroleast (use * mode: always))
    ;∀N.(∀M.M<N⊃NATNUM(F(M))∧1≤F(M))⊃N≤SUM(λK.F(K),N)
    (label strictly_increasing)

;other direction

11. (assume |(∀m.m<n⊃natnum f(m)∧1≤f(m))∧sum(λk.f(k),n)=n⊃(∀m.m<n⊃1=f(m))|)
    (label pfindhyp)

12. (assume |∀m.m<n'⊃natnum f(m)∧1≤f(m)|)
    (label pf_assume)

13. (derive |∀m.m<n⊃natnum f(m)∧1≤f(m)| (pf_assume transitivity_of_order successor1))
    (label pf0)

14. (ue ((numseq.|λk.f(k)|)(n.n)) sumsort *)
    ;NATNUM(SUM(λK.F(K),N))
    (label pfsort)
    ;deps: (PF_ASSUME)

15. (derive |natnum f(n)∧1≤f(n)| (pf_assume successor1))
    (label pf1)
    ;deps: (PF_ASSUME)

16. (assume |sum(λk.f(k),n')=n'|)
    (label pf_assume)

17. (rw * (open sum))
    ;SUM(λK.F(K),N)+F(N)=N'
    (label pf2)
    ;deps: (PF_ASSUME)

;the case of f(n)

18. (derive |n≤sum(λk.f(k),n)| (strictly_increasing pf0 pfsort))
    (label pf3)
    ;deps: (PF_ASSUME)

;use
;labels: ADD_ONE 
;(AXIOM |∀K N M.1≤K∧N'=M+K∧N≤M⊃1=K∧N=M|)

19. (ue ((k.|f(n)|)(n.n)(m.|sum(λk.f(k),n)|)) add_one 
      (pf1 pf2 pf3 pfsort))
    ;1=F(N)∧N=SUM(λK.F(K),N)
    (label pf4)
    ;deps: (PF_ASSUME)

;use the induction hypothesis

20. (derive |∀m.m<n⊃1=f(m)| (pfindhyp pf0 *))
    (label pf5)   
    ;deps: (PF_ASSUME PFINDHYP)

21. (derive |n0=n⊃1=F(n0)| pf4)
    ;deps: (PF_ASSUME)

22. (trw |∀m.m<n'⊃1=f(m)| (use less_succ_lesseq mode: exact) 
       (open lesseq) (use normal mode: always) pf5 *)
    ;∀M.M<N'⊃1=F(M)
    ;deps: (PF_ASSUME PFINDHYP)

23. (ci pf_assume)
    ;(∀M.M<N'⊃NATNUM(F(M))∧1≤F(M))∧SUM(λK.F(K),N')=N'⊃(∀M.M<N'⊃1=F(M))
    ;deps: (PFINDHYP)

24. (ci pfindhyp)

25. (ue (a |λn.(∀m.m<n⊃natnum f(m)∧1≤f(m))∧sum(λk.f(k),n)=n⊃(∀m.m<n⊃1=f(m))|)
             proof_by_induction *)
    ;∀N.(∀M.M<N⊃NATNUM(F(M))∧1≤F(M))∧SUM(λK.F(K),N)=N⊃(∀M.M<N⊃1=F(M))

26. (trw |∀f n.(∀m.m<n⊃natnum f(m)∧1≤f(m))∧sum(λk.f(k),n)=n⊃(∀m.m<n⊃1=f(m))| *)
    ;∀F N.(∀M.M<N⊃NATNUM(F(M))∧1≤F(M))∧SUM(λK.F(K),N)=N⊃(∀M.M<N⊃1=F(M))
;the pigeon hole principle on lists
    (wipe-out)
    (get-proofs pigeon prf ekl sys)

(proof pigeonlist)
;a fix
    (ue (a |λn.natnum sum(λm.mult(u,setseq m),n)|) proof_by_induction (open sum))
    ;∀N.NATNUM(SUM(λM.MULT(U,SETSEQ(M)),N))

1.  (assume |disjoint(setseq,length u)|)
    (label pl1)

;multiplicity less than length

2.  (ue ((u.u)(a.|un(setseq,length u)|)) length_mult)
    ;MULT(U,UN(SETSEQ,LENGTH U))≤LENGTH U
    (label pl2)

3.  (derive |sum(λm.mult(u,setseq(m)),length u)≤length u| 
            (mult_of_un_is_sum_mult pl1 pl2))
    (label pl3)

4.  (ue ((f.|λm.mult(u,setseq(m))|)(n.|length u|)) pigeonfact pl3 multfact)
    ;(∀M.M<LENGTH U⊃1≤MULT(U,SETSEQ(M)))⊃(∀M.M<LENGTH U⊃1=MULT(U,SETSEQ(M)))
    ;deps: (PL1)

;the pigeon hole principle on lists

5.  (ci pl1)
    ;DISJOINT(SETSEQ,LENGTH U)⊃
    ;((∀M.M<LENGTH U⊃1≤MULT(U,SETSEQ(M)))⊃(∀M.M<LENGTH U⊃1=MULT(U,SETSEQ(M))))